The invention relates to a method, a system and a computer program for comparing a first specification with a second specification, with the first specification and the second specification each covering at least two processes, each of which includes at least two events.
Computers are increasingly being used in a computer network, referred to as a computer system, in order to make it possible to use at least some of the services available in the computer system at different positions. In this context, communication between the individual computers, and independently of programs which follow one another on a computer, is an essential characteristic which allows efficient, fast and hence extremely economic operation, particularly due to the capability for concurrent processing.
On example of such a computer system is the Internet, which connects a large number of computers to one another. In this case, a number of processes which run independently of one another in a computer are in particular referred to as subscribers in the computer system.
When processes are being carried out or processed in parallel (concurrently), it is often possible for effects to occur which are difficult to predict, or are completely unpredictable, with regard to the interaction between the processes (see in particular, K. C. Tai, R. H. Carver: Testing of distributed programs; A. Zomaya (ed.): Handbook of Parallel and Distributed Computing; McGraw Hill; 1995; pp. 956–979.). Furthermore, in practice, it is impossible to test the entire computer system for all the possible options and states.
For each type of concurrence, it is often of critical importance to be able to state whether two concurrent processes have the same semantics. The sequence of the events that have occurred may (and also generally will) vary in each run. Nevertheless, these run sequences are semantically equivalent if the sequence changes occur only in the concurrent events. In a sufficiently large system, such as a comparison can be carried out only with very major effort, and is at the same time extremely susceptible to errors.